Musik

Herzlich willkommen.

Wir waren letztes Mal mittendrin unterbrochen worden.

Das heißt, wir sammeln mal wieder ein, was wir an Material angesammelt hatten.

Wir hatten bewiesen folgenden Satz.

Quatsch, nicht der SLD-Resolution, sondern Vollständigkeit der Resolution ohne eben diese ganzen Einschränkungen, die SLD-Resolution witzig bringt.

Und zwar ist das folgendermaßen formuliert, wir nehmen uns hier ein definites Programm P.

Wir nehmen uns hier ein Atom A, sodass A eine logische Konsequenz von P ist.

Vollständigkeitssätze sind ja immer derselben Natur, wenn etwas semantisch gesehen eine logische Konsequenz ist.

Das ist jetzt also eine Implikation zwischen Erfüllung von Formeln durch Modelle.

Dann bekommen wir auch eine syntaktische Herleitung hin.

In diesem Falle besteht die syntaktische Herleitung in dem, was wir einen Beweisbaum, oder genauer gesagt einen P-Beweisbaum genannt hatten.

Dann existiert ein P-Beweisbaum für A.

Wohlgemerkt in beiden Fällen, links und rechts des logischen Konsequenzzeichens, lesen wir hier implizit alle Formeln als allquantifiziert.

Gut, das hatten wir fertig bewiesen.

Dazu hatten wir ein Modell gebaut, das so ähnlich aussah wie das Erbraum-Modell, aber als Individuen im Grundbereich nicht mehr nur geschlossene, sondern beliebige Terme hatte.

Damit waren wir fertig gewesen. Es folgt als nächstes der Vollständigkeitssatz für die SLD-Resolution.

Ich schreibe noch einmal hin, was wir da eigentlich beweisen wollen.

Also folgender Satz, das ist jetzt Vollständigkeit der SLD-Resolution.

Dann nehmen wir uns hier ein definites Programm und eine Anfrage.

Wir nehmen an, dass es auf diese Anfrage eine Antwort gibt. Es bricht einem immer so ein bisschen das Hirn zu sagen, was es heißt, dass es auf diese Anfrage eine Antwort gibt.

Wohlgemerkt, die Anfrage ist was negiertes und dass wir eine Antwort bekommen, heißt, wir bekommen eine Substitution, für die wir das Gegenteil beweisen können.

Das heißt, wir haben eine Substitution Sigma mit der Eigenschaft, dass aus P als logische Konsequenz folgt, das aus P folgt, das allquantifiziert gilt nicht Q Sigma.

Wenn das der Fall ist, dann sagt der Vollständigkeitssatz, bekommen wir eine SLD-Resolution, deren Antwort eventuell nicht identisch ist zu Sigma, aber zumindest besser als Sigma.

Das ist ja wohl reichen. Das heißt also Folgendes, es gibt eine SLD-Resolution, eine SLD-Herleitung Delta, die fängt an mit Q, Q nennen wir gleichzeitig Q0, geht weiter mit irgendeiner Regelanwendung D0 zu Q1 und so weiter.

Das endet bei der leeren Klausel, das heißt, diese Herleitung ist eine Refutation. Weil sie eine Refutation ist, bekommen wir eine Antwort aus ihr.

Diese Antwort ist eine Substitution. Diese Substitution, die wir bekommen, die ist eben besser als, also mindestens so gut wie oder besser als Sigma.

Was wir daran erkennen, dass wir, wenn wir die Substitution auf unser Q loslassen, dass wir dann das nochmal spezialisieren können zu Q Sigma.

Also Q Sigma von Delta Gamma gleich Q Sigma für ein Gamma. Das heißt also Q Sigma von Delta, also die Substitution, die wir als Antwort kriegen, losgelassen auf die eigentliche Anfrage, ist zwar nicht identisch zu Q Sigma, aber sie ist im Zweifelsfalle allgemeiner als Q Sigma.

Das heißt, wir kommen Q Sigma daraus durch Spezialisierung. So, das ist der Zielsatz, den wir jetzt mit Hilfe des obenstehenden Satzvollständigkeits der Resolution beweisen.

Wir hatten auch schon angefangen.

So, hier kommt der Beweis, so wie wir den letztes Mal begonnen hatten.

Also, wir zunächst mal unsere Anfrage. Die Anfrage ist ja eine Zielklausel, bestehend aus einem Stapel Atome, die negiert werden. Das heißt also, wir nehmen hier Q gleich Pfeil a1 bis a n.

Das ist also die Negation der Konjunktion dieser a1 bis a n. Hier oben haben wir nochmal eine Negation davor. Das heißt, diese beiden Negationen heben sich gegenseitig wieder auf.

Das heißt, wir haben das aus P oder für alle P als logische Konsequenz folgt für alle a1 Sigma und a n Sigma.

Und das können wir wiederum auseinandernehmen. Wir haben hier eine Konjunktion unter einem Al-Quantor. Konjunktion und Al-Quantor können wir vertauschen.

Das heißt, hieraus folgt wiederum für alle P, hat als logische Konsequenz für alle a i Sigma, das Ganze für i gleich 1 bis n.

Hier schlägt dann zu der schon bewiesene Vollständigkeitssatz für die Resolution. Das hier sind ja alles Atome. Auch wenn ich substituiere, bleibt es noch ein Atom.

Atom heißt nichts weiter, als dass ich ein Prädikatensymbol habe und darunter irgendwelche Terme als Argumente. Das bleibt auch so, wenn ich da rein substituiere.

Das heißt, diese a i Sigma sind Atome. Und weil sie aus P logisch folgen, haben sie also P-Beweisbäume nach dem vorigen Satz.

Also, die a i Sigma haben P-Beweisbäume nach dem vorigen Satz.

Wir gehen jetzt hin und zählen die Anzahl Knoten in diesem Beweisboden. So weit waren wir schon.

Da kommt eben irgendeine Zahl raus, n. Also, die Gesamtzahl Knoten, die nennen wir n.

So, n wird jetzt die Länge der SLD-Herleitung, die wir konstruieren.

Ich lasse jetzt hier ein bisschen Platz. Eine SLD-Herleitung, die folgendermaßen aussieht, Delta gleich, die fängt an bei Q gleich Q0, macht irgendeinen Schritt D0 nach Q1 usw., landet bei Qn.

Qn ist die leere Klausel. Das heißt, das ist eine SLD-Refutation.

So, die konstruieren wir induktiv. Induktiv heißt, wir nehmen an, sie sei bis Qi konstruiert und wir konstruieren dann einen Schritt weiter.

Natürlich ist nicht Teil der Induktion, dass die letzte Klausel immer leer ist. Das ist erst im letzten Schritt der Fall.

Also, das konstruieren wir induktiv mit einer etwas komplizierten Invariante. Um die Invariante ausdrücken zu können, müssen wir uns mehr Bezeichner verschaffen.

Und zwar brauchen wir zunächst mal Namen für die Substitutionen, die hier zwischendurch stattfinden, um die Regeln tatsächlich anwenden zu können.